\begin{tabbing}
EVal{-}atom{-}free\=\{i:l\}\+
\\[0ex]($X$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$i$:Id, $x$:Id. atom{-}free\{1:n\}(Type\{i\}; ((($X$.2.2.2.2.2).1)($i$,$x$))))\+
\\[0ex]\& ($\forall$$i$:Id, $k$:Knd. atom{-}free\{1:n\}(Type\{i\}; ((($X$.2.2.2.2.2.2.2.2.2).1)($k$,$i$))))
\-
\end{tabbing}